perm filename CLASS.83[206,JMC] blob
sn#681011 filedate 1983-09-29 generic text, type C, neo UTF8
COMMENT ā VALID 00002 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 \magnify{1200}
C00007 ENDMK
Cā;
\magnify{1200}
\output{\shipout\box255}
\newfont cmb12 \is \title
\def\.#1{\hbox{\tt #1}}
\def\xskip{\hskip7pt plus3pt minus4pt}
\let\yskip=\smallskip
\def\data#1:{\par\yskip\hangindent 2em\noindent{\bf #1: }\ignorespace}
\ctrline{\:\title CS 206---Recursive Programming and Proving}
\vskip 10pt
\ctrline{Class information}
\vskip 10pt
\data Time and place: Class meets in ERL 320 from 1:15 to 2:30 on Tuesdays and
Thursdays. Lectures are also broadcast to TV students.
\data Instructor: Prof.\ John McCarthy. Office is Margaret Jacks Hall
(Building 460) room 356, phone 497-4430. Available most afternoons; see
Fran Larson (MJH 358, phone 497-2800) to make an appointment.
\data Teaching Assistant: Joe Weening. Office is MJH 353, phone 497-1517.
Office hours Monday and Thursday from 2:30 to 4:00. Computer address
\.{W.Weening} at \.{LOTSB}, or \.{JJW} at \.{SU-AI} (from ARPAnet machines).
\data Textbook: {\sl LISP: Programming and Proving}, by John McCarthy and
Carolyn Talcott. Available in the Stanford bookstore.
\data Other books: MacLisp Reference Manual, available in the Stanford
bookstore.\xskip ``A@Summary of MacLisp Functions and Flags,'' by David S.
Touretzky, Carnegie-Mellon University, will be sold in class.\xskip
The {\sl Lisp Machine Manual\/} provides a better description of MacLisp
than the MacLisp manual. Copies of this will also be sold in class to
those interested.\xskip ``EKL Reference Manual'' will be distributed in class
when we begin using the EKL interactive proof-checker.
\data Computer use: CS 206 will use the LOTSB computer, which has terminals
in the CERAS building. See the handout ``Using MacLisp at LOTS'' for more
information. Students with access to other computers that have LISP may use
those machines, except that the research facilities of the Computer Science
Department (SCORE, SAIL, or other machines funded by research grants) may
{\sl not\/} be used for class assignments. EKL will be available at LOTSB.
\data Assignments: Homework problems will be given at various times throughout
the class. Some of these will involve writing simple LISP programs in external
notation and running programs on the computer. Later assignments will include
simple proofs of program correctness, and checking these proofs using EKL.
\data Exams: There will be an in-class midterm exam on Thursday, November 4.
The final exam is scheduled for Tuesday, December 14 at 7:00 p.m.
\data Project: Near the end of the course, there will be an optional term
project, which will be a more substantial program or proof than those done in
class. Projects will be due on the day of the final exam. More details will be
given later.
\data Grading: Grades will be based on the assignments, midterm, final, and
project. A project is not required to pass the course, or even to get a B
if the assigment and exam grades are good enough. However, if you wish to
get some flavor of A then doing a good term project is necessary.
\vfill\end